M.rframe(A.effect f of k on y)
== xdom(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M)))))))))))). 

== L=1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M)))))))))))(x)  
== Ldeq-member(KindDeq;k;L)
==  (s1, s2:A.state, v:A.da(k). (s1  s2 mod x)  f(s1,v) = f(s2,v)) 

latex

---

clarification:

M.rframe(A.effect f of k on y)
== fpf-all(Id;
== fpf-all(IdDeq;
== fpf-all(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M)))))))))));
== fpf-all(x,L.(deq-member(KindDeq;k;L)
== fpf-all( (s1:A.state, s2:A.state, v:A.da(k).
== fpf-all( (ma-x-equiv(A;x;s1;s2)  f(s1,v) = f(s2,v)  fpf-cap(1of(A);IdDeq;y;Void)))) 

latex

Definitions	xdom(f). v=f(x)   P(x;v), Id, 2of(t), P  Q, b, deq-member(eq;x;L), KindDeq, M.state, x:A. B(x), M.da(a), P  Q, (s1  s2 mod x), s = t, f(x)?z, 1of(t), IdDeq, Void, f(a)
FDL editor aliases	ma-rframe-ef